w:World, a, b:E. w_locle(w;a;b)  Prop 

latex

Definitions	World, t  T, x:A. B(x), E, w-pred(w;e), x.A(x), P  Q, pred(e), s = t, first(e), b, A, Type, Prop, A & B, x:AB(x), R^*, f(a), x f y, w_locle(w;x;y)
Lemmas	rel star wf, not wf, assert wf, first wf, pred wf, w-pred wf, w-E wf, world wf